\subsection{Formal model}
\begin{center}
	\emph{This applies to section 10 and 20, the section 12 does not apply to our model.\\
		Note: The CPN file is attached in the zip-file, below are screenshots of the model and its problems.}
\end{center}

For this problem we have chosen to use a CPN diagram. We have done this because the given assignment has a simple and clear problem, which can easily be expressed using CPN tools.\\
\\
The model starts with a token generator to simulate companies bidding on available orders. To keep the model simple we decided to randomly generate discrete variables within only 1 and 9 in order to compare these more easily with each other. Additionally we have added timing to the model to show faults that can occur due to the locking system.\\
\\
According the specification, only one bid can be processed at the same time, therefore we simulated a lock system similar to the one described in the specification. Once the bid has been processed by the system, it will be checked by a checking system (and if it is the first bid in the entire system, it will immediately be stored to initialize our system). 
New bids will then be checked by our checking system.\\
\\
\texttt{Company\_ID} of new bids will be compared by the \texttt{Company\_ID}'s of bids that are currently in storage. If the \texttt{Company\_ID} of the new bid (variable $a$) is unique, the bid will be stored in the storage. If this is not the case and the \texttt{Company\_ID} of the new bid (variable $a$) is equal to a \texttt{Company\_ID} of the bid in our storage (variable $m$), the new bid will overwrite the old bid and the old bid will be stored in a separate "deleted-bid storage". This happens in order to ensure that the company only has one current bid in the storage system as specified by the assignment.\\
\\
Now we will run simulations of the real world system using our CPN model to find out if the expected errors could indeed occur, and in which way. The results of this are described here and can be seen in the images included below.\\
\\
In the second image of the model there is a simulation of the unique \texttt{Company\_ID} fault causing errors highlighted by our CPN model. Since the string $(a,b,c)$ represents the $(\texttt{Company\_ID},$ \texttt{Order\_ID} $,\texttt{price})$, it is possible to see that some bids have been moved to the "deleted-bid storage" while they should preferably still be active. Specifically, this shows a bid that company \#3 had previously placed on order \#6, but was removed after it placed a bid on the completely different order \#8. Now order \#6 is being fulfilled by the different company \#6, who placed a higher bid than company \#3 did, so this causes Floral Direct to get a worse deal than it should (it now pays \euro4,- for the order, instead of the \euro1,- offered before).\\
\\
A second error due to the same unique \texttt{Company\_ID} flaw is highlighted in the third image. This time it shows two orders, \#3 and \#4, being left unfulfilled even though a company with ID \#6 had actually placed bids on these orders. The problem is that this company has afterwards placed a bid on a completely different order causing the system to undesirably delete previous bids on these different orders. Since no other company has placed any bids on these orders they are now left completely unfulfilled.\\
\\
Other than the unique \texttt{Company\_ID} flaw we defined and simulated first, we have since been able to implement timing into our model to prove a second flaw possibly causing the real world problems for Floral Direct. Specifically, by having a bid stuck in the locking system at the time of fulfillment of an order it is not being considered by the system, even though the bid was placed in time. The simulation of this in the fourth image shows company \#2 having placed the best bid on order \#8 just in time for the 30 minute closing time of an order. However, since it has not been released by the lock yet the system does not find it when going through the bids table. This causes the order to be left unfulfilled since there is no other bid on that order in the table at the time. Finally, this locking system flaw could similarly cause a worse bid becoming the winner if the best bid is still stuck in the lock. So, just like the \texttt{Company\_ID} error the timing error can also cause both of the problems our client is experiencing.\\
\\
When looking back on the use of our model we have learned the following:\\
Our formal model took up the assumption that 40\% of all flower stores are partners with Floral Direct. Furthermore we also took the assumption that Floral Direct roughly takes a 40\% marketshare of all online flower orders. These assumptions provide us with enough information to create a model that represented the errors occurring in the order process of Floral Direct. Due to the rough calculations employed here, we were able to reproduce and verify the internal error of the order process of  Flower Direct. By focusing solely on the Dutch market we narrowed the product to be distributed in a more concrete region. The model is of a  smaller scale than the order system of Flower Direct, nonetheless it gave us a rather thorough understanding of the issues in the ordering system.

\clearpage
\begin{center}
	\includegraphics[width=0.8\linewidth]{_new_CPN_clean} \\
	\bf{1. Formal model in CPN before simulation.}
	\linebreak
	\linebreak
	\includegraphics[width=0.8\linewidth]{_new_CPN_ID_worse_bid_error} \\
	\bf{2. Simulating a more expensive winner due to \texttt{Company\_ID} fault.}
	\clearpage
	\includegraphics[width=0.8\linewidth]{_new_CPN_ID_unfulfilled_error} \\
	\bf{3. Simulating an unfulfilled order due to \texttt{Company\_ID} fault.}
	\linebreak
	\linebreak
	\includegraphics[width=0.8\linewidth]{_new_CPN_timed_unfulfilled_error} \\
	\bf{4. Simulating an unfulfilled error due to locking system fault.}
\end{center}